COMMENT ⊗   VALID 00009 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	basic facts about arithmetic and proofs by Bellin
C00008 00003	inductive principles
C00010 00004	PROOFS
C00011 00005	commutativity of addition
C00012 00006	commutativity of inductively defined multiplication 
C00013 00007	distributivity of multiplication over addition (cont'd)
C00014 00008	plus cancellation
C00015 00009	times cancellation (condt'd)
C00016 ENDMK
C⊗;
;basic facts about arithmetic and proofs by Bellin

(wipe-out)  
(proof natnum)

(decl lessp (type: |ground⊗ground→truthval|) (syntype: constant) (infixname: <)
      (bindingpower: 920))
(decl add1 (type: |ground→ground|) (syntype: constant) (postfixname: |'|)
      (bindingpower: 975))
(decl plus (infixname: |+|) (type: |ground⊗ground⊗ground*→ground|) (syntype: constant)
      (associativity: both) (bindingpower: 930))    
(decl times (type: |ground⊗ground⊗ground*→ground|) (syntype: constant)
      (infixname: |*|) (associativity: both)(bindingpower: 935))

(decl (i j k n m) (sort: natnum) (type: ground))
(decl (a b c set) (type: |ground→truthval|))

;needed axioms on order

(axiom |∀n.¬n<n|)
(label irreflexivity_of_order)

(axiom |∀n m k.n<m∧m<k⊃n<k|)
(label transitivity_of_order)

(axiom |∀n.¬n<0|)
(label zeroleast1)

;successor and order

(axiom |∀n.natnum(n')|)
(label simpinfo)

(axiom |∀n.n<n'|)
(label successor1) (label succfacts)

(axiom |∀n m.¬n<m⊃m<n'|)
(label successor2) (label succfacts)
 
(axiom |∀n m.n'<m'≡n<m|)
(label successorless) (label succfacts)

(axiom |∀n m.(n'=m')≡(n=m)|)
(label successoreq) (label succfacts)

(axiom |∀n.¬n=0⊃0<n|)
(label zeroleast2) (label succfacts)
 
(axiom |∀n.0<n'|)
(label zeroleast3) (label succfacts)

(axiom  |∀n.¬(n'=0)|)
(label zero_not_successor) (label succfacts)

;definition of predecessor

(decl pred (type: |ground→ground|) (syntype: constant))
(defax pred |∀n.pred(n')=n|)
(label simpinfo)

(axiom |∀n.natnum pred n|)
(label simpinfo)

;addition

(defax plus |∀n k.0+n=n∧k'+n=(k+n)'|)
(label simpinfo) (label plusfacts) (label plusdef)

(axiom |∀n m.natnum(n+m)|)
(label simpinfo)

(axiom |∀n.n+0=n|)
(label simpinfo) (label plusfacts)

(axiom |∀n.1+n=n'∧n+1=n'|)
(label simpinfo) (label plusfacts) (label plusdef1)

(axiom |∀n k.n+k'=(n+k)'|)
(label simpinfo) (label plusfacts)

(axiom |∀n k m.(k+m=k+n)≡(m=n)|)
(label lpluscan) (label plusfacts)

(axiom |∀n k m.(m+k=n+k)≡(m=n)|)
(label rpluscan) (label plusfacts)

(axiom |∀n k.n+k=0≡n=0∧k=0|)
(label addtozero) (label plusfacts)

;the effect of the following axiom is to force sums in basically normal
;form: the "simpler" terms will come first

(axiom |∀k n.k+n=n+k|)
(label commutadd) (label plusfacts)

;multiplication

(defax times |∀n k.0*n=0∧n'*k=(n*k)+k|)
(label simpinfo) (label timesfacts) (label timesdef)

(axiom |∀n m.natnum(m*n)|)
(label simpinfo)
  
(axiom |∀n.n*0=0∧1*n=n∧n*1=n|)
(label simpinfo) (label timesfacts)

(axiom |∀n k.n*k'=n*k+n|)
(label timsucc) (label timesfacts)

(axiom |∀n k m.¬k=0⊃((k*m=k*n)≡(m=n))|)
(label ltimescan) (label timesfacts)

(axiom |∀n k m.¬k=0⊃((m*k=n*k)≡(m=n))|)
(label rtimescan) (label timesfacts)
 
(axiom |∀n m.n*m=m*n|)
(label commutmult) (label timesfacts)

(axiom |∀n k.¬n=0⊃n*k=0≡k=0|)
(label ltimestozero) (label timesfacts)

(axiom |∀n k.¬n=0⊃k*n=0≡k=0|)
(label rtimestozero) (label timesfacts)

;distributivity

(axiom |∀n k m.n*(k+m)=n*k+n*m|) 
(label ldistrib) (label timesfacts) (label plusfacts)

(axiom |∀n m k.(m+k)*n=m*n+k*n|)
(label rdistrib) (label timesfacts) (label plusfacts)
;inductive principles

(proof induction)

(axiom |∀a.a(0)∧(∀n.a(n)⊃a(n'))⊃(∀n.a(n))|)
(label proof_by_induction)

(decl npars (type: |ground*|))
(decl ndf (type: |ground⊗ground*→ground*|))
(decl zcase (type: |ground*→ground|))
(axiom
 |∀ndf zcase ndef.(∃fun.(∀npars n.fun(0,npars)=zcase(npars)∧
                                  fun(n',npars)=ndef(n,fun(n,ndf(n,npars)),npars)))|)
(label inductive_definition)

;the following is a form of double induction

(axiom |∀a2.(∀n m.a2(0,n)∧a2(n,0)∧(a2(n,m)⊃a2(n',m')))⊃∀n m.a2(n,m)|)
(label proof_by_doubleinduction)

;general definitional principle for inductive functions

(decl (arb arb1 arb2) (type: |?arbitrary|))
(decl indfn (type: |ground⊗@arb→@arb|))
(decl (def_fun) (type: |ground→@arb|))

;this is the primitive recursive schema for definition on  ALL
;higher type functionals:
;note the use of the variable type in declarations;
;in this way we can specialize to ANY type.

(axiom
 |∀indfn arb.∃def_fun.∀n.def_fun(0)=arb∧def_fun(n')=indfn(n,def_fun(n))|)
(label high_order_natnum_definition)

;well-foundedness

(axiom |¬∃desc.∀n.desc(n')<desc(n)|)
(label infinite_descent)

(save-proofs natnum)
;PROOFS
;commutativity of addition
(wipe-out)
(get-proofs natnum)
(proof commutaddition)
;3s
(unlabel simpinfo plusfacts) ;delete plusfacts from simpinfo temporarily

(ue (a |λn.∀k.n+k'=(n+k)'|) proof_by_induction (open plus))
;∀N K.N+K'=(N+K)'
(label plushelp)

(ue (a |λn.n+0=n|) proof_by_induction (open plus))
;∀N.N+0=N
(label pluszero)

(ue (a |λk.∀n.n+k=k+n|) proof_by_induction  (open plus) (use plushelp pluszero))
;∀N N3.N3+N=N+N3
(label commutadd)
;commutativity of inductively defined multiplication 
;4s

(wipe-out) 
(get-proofs natnum)
(proof multip)

(unlabel simpinfo timesfacts) ;delete this stuff temporarily

(ue (a |λk.0*k=k*0|) proof_by_induction (part 1 (open times)))
;∀N.0*N=N*0
(label zerocase)

(ue ((a.|λn.(∀k.n*k'=n*k+n)|)) proof_by_induction
    (part 1 (use commutadd) (open times)))
;∀N K.N*K'=N*K+N
(label littlehelp)

(ue (a |λk.∀n.n*k=k*n|) proof_by_induction 
    (open times) (use littlehelp mode: always) (use zerocase))
;∀N N3.N3*N=N*N3
(label commutmult)

(label simpinfo timesfacts) 
;distributivity of multiplication over addition (cont'd)
;2s
(proof multip)

;adding these labels to simpinfo has the effect of "normalizing"
;expressions involving addition and multiplication:
;the terms of a sum are listed in the order of their complexity, with
;the simplest ones coming first

(label simpinfo commutmult commutadd)
(unlabel simpinfo ldistrib rdistrib)

(ue (a |λn.∀k m.n*(k+m)=n*k+n*m|) proof_by_induction
    (open times) (use littlehelp mode: always))
;∀N K M.N*(K+M)=K*N+M*N

(trw |∀n m k.(m+k)*n=m*n+k*n| ldistrib *)
;∀N M K.(M+K)*N=M*N+K*N
;plus cancellation
;2s
(wipe-out)
(get-proofs natnum)
(proof cancel)
 
(unlabel simpinfo lpluscan rpluscan ltimescan rtimescan)
(unlabel simpinfo commutadd commutmult)
(label simpinfo succfacts)
 
(ue (a |λk.∀n m.(k+n=k+m)≡(n=m)|) proof_by_induction)
;∀N N3 M.N+N3=N+M≡N3=M

(trw |∀n m k.(n+k=m+k)≡(n=m)| (use * commutadd))
;∀N M K.N+K=M+K⊃N=M
 
(label simpinfo lpluscan rpluscan)

(ue (a |λk.∀n.(k+n=0)≡(k=0∧n=0)|)  proof_by_induction)
;∀N N4.N+N4=0≡N=0∧N4=0
(label addtozero) (label simpinfo)
;times cancellation (condt'd)
;6s

(ue (a |λk.∀n.¬k=0⊃((k*n=0)≡(n=0))|) proof_by_induction
    (open times) (use addtozero mode: always))
;∀N N8.¬N=0⊃N*N8=0≡N8=0
(label ltimestozero) (label simpinfo)

(ue (a2 |λn m.∀k.¬k=0⊃((n*k=m*k)≡(n=m))|) proof_by_doubleinduction 
    (open times) (use commutmult))
;∀N M K.¬K=0⊃K*N=K*M≡N=M